1. Field of the Invention
The present invention generally relates to design of provably correct arrays in complex logic and memory systems implemented in very large scale integrated (VLSI) circuits and, more particularly, to a hardware design technique that allows checking the design system language (DSL) specification of large macros with embedded arrays and registers.
2. Background Description
As the number of transistors used for complex logic and memory increases on a central processing unit (CPU) chip, the verification of intended functionality versus the actual functionality becomes a major task. To illustrate this point, many top level circuits as well individual circuits need to be evaluated with respect to static function, timing, testability of scan chain and manufacturability. As a result, a complete verification of logic and memory on a CPU chip is a necessity for low development cost and short design delivery cycles.
In the verification process, user-defined functions are checked at gate or transistor levels. The user defined functions are coded in Boolean algebra. The checking is done from top to bottom, which is termed as hierarchical.
The functional behavior of a high level system (e.g., a CPU chip) is validated by first modeling at an abstract level. This abstract level is simulated using a predesigned environment, such as running software applications or running a random set of processor instructions. Once the desired performance is achieved, the abstract model becomes the definition of the intended system function. This is often referred to as the "golden model".
The golden model can be synthesized to achieve gate levels description of the intended function. Conventionally, the synthesis is done automatically. The automation may limit the possible implementation of styles as it can grab fixed cells from the designated libraries. This may not result in optimization of area, timing and power. However, the synthesis maintains the functionality of the abstract specification, provided that the algorithms applied are correct. As a result, the functional verification is performed on the final design to confirm the validity of the synthesis algorithms.
Normally, the synthesis procedure is adopted for random logic especially when the synthesis rules are easily available (e.g., libraries, timing, pin information, etc.). It is easier to create libraries for static circuits. However, many times these limit the performance. As a result, a combination of dynamic and static circuits are used in to improve performance. In addition, circuits are tuned to the performance, and custom layouts to reduce area and power are heavily used. This is typically termed as custom or semi-custom (mixed static and dynamic) design. The custom design process is normally done independent of the "golden model". As a result, a separate functional verification step for the final implementation is very crucial. There are two approaches to custom circuit verification.
In the first approach, the switch level representation of complementary metal oxide semiconductor (CMOS) circuits is stimulated using the system level stimuli. The smaller granularity of this model causes a significant increase in simulation complexity. This reduces total number of patterns which in turn reduce the verification coverage. To resolve this problem, gate level model is abstracted from the transistor representation and by using hardware accelerators for switch level simulation. In spite of these developments these repeated functional simulations on the circuit level is highly time-intensive and difficult for user friendly applications.
A method to formally verify memory circuits based on the second approach compares transistor level logic (decoder, resets etc.) and memory and high level specification. Even though the specification is listed "fully functional", at the transistor level design may result in errors due to limitations on the test pattern coverages. Thus, by checking transistor level design with formal specification can produce robust design methodology. The goal here is to achieve substantial pattern coverage across the memory design.